|
: ''This article describes Kripke structures as used in model checking. For a more general description, see Kripke semantics''. A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke,〔Kripke, Saul, 1963, “Semantical Considerations on Modal Logic,” Acta Philosophica Fennica, 16: 83-94〕 used in model checking〔Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science. Springer Berlin Heidelberg, p. 1-26.〕 to represent the behavior of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures. ==Formal definition== Let ''AP'' be a set of ''atomic propositions'', i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al.〔Clarke, Grumberg and Peled: "Model Checking", page 14. The MIT Press, 1999.〕 define a Kripke structure over ''AP'' as a 4-tuple ''M'' = (''S'', ''I'', ''R'', ''L'') consisting of * a finite set of states ''S''. * a set of initial states ''I'' ⊆ ''S''. * a transition relation ''R'' ⊆ ''S'' × ''S'' such that ''R'' is left-total, i.e., ∀s ∈ ''S'' ∃s' ∈ ''S'' such that (s,s') ∈ ''R''. * a labeling (or ''interpretation'') function ''L'': ''S'' → 2''AP''. Since ''R'' is left-total, it is always possible to construct an infinite path through the Kripke structure. A deadlock state can be modeled by a single outgoing edge back to itself. The labeling function ''L'' defines for each state ''s'' ∈ ''S'' the set ''L''(''s'') of all atomic propositions that are valid in ''s''. A ''path'' of the structure ''M'' is a sequence of states ρ = s1,s2,s3,... such that for each i > 0, ''R''(si, si+1) holds. The ''word'' on the path ρ is sequence of sets of the atomic propositions ''w''=''L''(s1),''L''(s2),''L''(s3),..., which is an ω-word over alphabet 2''AP''. With this definition, a Kripke structure may be identified with a Moore machine with a singleton input alphabet, and with the output function being its labeling function. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Kripke structure (model checking)」の詳細全文を読む スポンサード リンク
|